| Definitions | t  T, Valtype(da;k), State(ds),  x:A. B(x),   x. t(x), Knd, IdLnk, x:A  B(x), Id, Type, rcv(l,tg), Void, f(x)?z, type List, x:A  B(x), a:A fp B(a), Top, t.1, ||as||, P   Q, False,  A, P & Q, A  B, i j < k,  , {x:A| B(x)} , {i..j }, a < b,  , t.2,  , x dom(f),  b, x.A(x), l[i], f(a), s = t,  , #$n, deq-member(eq;x;L), left + right, P  Q, x,y. t(x;y), xdom(f). v=f(x) P(x;v), z != f(x) P(a;z), <a, b>, product-deq(A;B;a;b), map(f;as), (x l), IdLnkDeq, KindDeq, locl(a), IdDeq, MsgA, M.ds(x), M.dout(l,tg), (s1  s2 mod x), M.da(a), M.state, M.rframe(A.sends tfL of k on l), M.bframe(k sends on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B) |